k:Knd, l:IdLnk, ds:x:Id fp Type, da:a:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
xdom(ds). A=ds(x)   A
 kdom(da). A=da(k)   A
 xdom(ds). A=ds(x)   AtomFree(Type;A)
 kdom(da). A=da(k)   AtomFree(Type;A)
 Feasible(with declarations 
 ds:ds
 da:da
 k(v) sends f s v on link l) 

latex

Definitions

t  T, P  Q, x:A. B(x), Type, Knd, (x  l), x:AB(x), f(a), A, KindDeq, P  Q, Dec(P), left+right, x:AB(x), P & Q, P  Q, b, f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), AtomFree(T;x), a:A fp B(a), 1of(t), Id, type List, 2of(t), IdLnk, false, <a,b>, IdLnkDeq, product-deq(A;B;a;b), eqof(d), p  q, False, Void, rcv(l,tg), x.A(x), x. t(x), f(x)?z, Valtype(da;k), State(ds), map(f;as), deq-member(eq;x;L), IdDeq, z != f(x)  P(a;z), M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Feasible(M), mk-ma, , x : v, with declarations ds:dsda:dak(v) sends f s v on link l, Top, {x:A| B(x) }, Prop, x,y. t(x;y), nat-deq-aux, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, AB, , , Atom, prod-deq(A;B;a;b), proddeq(a;b), sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b)

Lemmas

atom-free wf, fpf-all wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, id-deq wf, deq-member wf, map wf, pi1 wf, ma-state wf, ma-valtype wf, fpf-cap wf, rcv wf, false wf, Id wf, assert wf, bor wf, eqof wf, product-deq wf, idlnk-deq wf, bfalse wf, IdLnk wf, assert-deq-member, Kind-deq wf, not wf, l member wf, Knd wf